<html>
<head>
    <title>lean.js minimal working example</title>
    <meta charset="utf-8">
</head>
<body>

<p>Small example of using lean.js</p>

<pre id="output"></pre>

<script type="text/javascript">
var myTimer = null;
function now () { return (new Date()).getTime(); }
function startTimer () { myTimer = now(); }
function checkTimer () { return '(took ' + (now() - myTimer) + 'ms)'; }

var outputElement = document.getElementById("output");
function outputLog(msg) {
    console.log(msg);
    outputElement.appendChild(document.createTextNode(String(msg) + "\n"));
}

/*
 * "Module" must be initialized before the <script> tag for lean.js.
 * The lean.js script populates Module with compiled Lean code,
 * but it needs to know about the parameters below or it will throw errors.
 */
outputLog('--- Loading Lean VM...'); startTimer();
Module = { };
Module.TOTAL_MEMORY = 64 * 1024 * 1024;
Module.noExitRuntime = true;
Module.print = function(text) { outputLog(text); };
Module.printErr = function(text) { console.log("STDERR " + text); };
Module.preRun = [
    function () {
        outputLog('--- Lean VM loaded. ' + checkTimer());
        outputLog('--- Running Lean VM...'); startTimer();
    }
];
Module.postRun = function () {
    outputLog('--- Lean VM has been run. ' + checkTimer());
}
</script>

<!-- Import the Lean javascript module generated by emscripten. -->
<script src="lean_js.js" type="text/javascript" charset="utf-8"></script>

<script type="text/javascript" charset="utf-8">

outputLog('--- Calling lean_init()...'); startTimer();
Module.lean_init();
outputLog('--- lean_init() complete. ' + checkTimer());

outputLog('--- Syncing test input...'); startTimer();
testfile = ''
         + 'variables p q r s : Prop\n'
         + 'theorem my_and_comm : p ∧ q ↔ q ∧ p :=\n'
         + 'iff.intro\n'
         + '  (assume Hpq : p ∧ q,\n'
         + '    and.intro (and.elim_right Hpq) (and.elim_left Hpq))\n'
         + '  (assume Hqp : q ∧ p,\n'
         + '    and.intro (and.elim_right Hqp) (and.elim_left Hqp))\n'
         + 'check @nat.rec_on\n'
         + 'print "end of file!"\n';
outputLog( testfile );
 var msg = JSON.stringify({
     seq_num: 0,
     command: "sync",
     file_name: "test.lean",
     content: testfile,
 });
 var len = Module.lengthBytesUTF8(msg) + 1;
 var msgPtr = Module._malloc(len);
 Module.stringToUTF8(msg, msgPtr, len);
 Module.lean_process_request(msgPtr);
outputLog('--- Sync complete. ' + checkTimer());
outputLog('--- Syncing test input...'); startTimer();
 Module.lean_process_request(msgPtr);
 Module._free(msgPtr);
outputLog('--- Sync complete. ' + checkTimer());

outputLog("--- Finished.");

</script>
</body>
</html>
